meta-theoretic operation

An operation we use in [[Programming Language Theory]] in the specification of our language, that are not constructs of the language we are defining.